\documentclass{article}

\usepackage{AMMALanguages}

\begin{document}

\begin{lstlisting}[style=AMMA, language=Maude, numbers=none]
(mod UNORDERED-CHANNEL is
  sorts Nat NatList Msg Conf State .
  subsort Msg < Conf .
  op 0 : -> Nat [ctor] .
  op s : Nat -> Nat [ctor] .
  op nil : -> NatList [ctor] .
  op _;_ : Nat NatList -> NatList [ctor] .   *** list constructor
  op _@_ : NatList NatList -> NatList .      *** list append
  op `[_`,_`] : Nat Nat -> Msg [ctor] .
  op ack : Nat -> Msg [ctor] .
  op null : -> Conf [ctor] .
  op __ : Conf Conf -> Conf [ctor assoc comm id: null] .
  op `{_`,_|_|_`,_`} : NatList Nat Conf NatList Nat -> State [ctor] .

  vars N M J K : Nat .      var  C : Conf .
  vars L P Q : NatList .

  eq nil @ L = L .          eq (N ; L) @ P = N ; (L @ P) . 

  rl [snd]: {N ; L, M | C | P, K} => {N ; L, M | [N, M] C | P, K} .     
  rl [rec]: {L, M | [N, J] C | P, J}  
    => {L, M | ack(J) C | P @ (N ; nil), s(J)}  .
  rl [rec-ack]: {N ; L, J | ack(J) C | P, M}  => {L, s(J) | C | P, M} .
endm)
\end{lstlisting}

\end{document}